es:ES, L:(Id List). fischer(L)  (e1, e2:E. Try(e1)  Try(e2)  Dec(e1 <f e2)) 

latex

Definitions	s = t, Id, loc(e), f-rel{$z,$wanted}(es;L;e1;e2), False, x:A.B(x), left + right, (e <loc e'), P  Q, P  Q, P  Q, Type, Dec(P), e loc e' , a = b, b, let x,y = A in B(x;y), E, t.1, fischer(L), type List, ES, x:A  B(x), , the rcv(wanted message from e1 to j), t  T, (x  l), x:A. B(x), x:AB(x), A, P  Q, Try(e), P & Q
Lemmas	l member subtype, es-loc wf, f-wanted wf, Id wf, not wf, decidable es-le, eq id wf, assert wf, assert-eq-id, not functionality wrt iff, es-le wf, es-E wf, es-locl wf, decidable cand, decidable not, decidable equal Id, event system wf, fischer wf, f-try wf